package controlGraph;

import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.Map;
import java.util.Queue;

/**
 * @author Administrator
 *
 */
public abstract class Statement {

	private static ArrayList<Statement> statements = new ArrayList<Statement>(50);
	public static store zigma= new store();
	public static ArrayArith rules = new ArrayArith();
	private static int last_num = 0;
	protected int label;
	protected String labelName;

	public Statement() {
		label = last_num++;
		statements.add(this); // I'm not sure that the indexes are guaranteed to be right
	}

	public abstract void visitSuccessors(store zigma, ArrayArith rules);

	/*
	 * { for(Successor s : succs) { ArrayList<String> tmpAxioms = new ArrayList<String>(axioms);
	 * tmpAxioms.addAll(s.axioms); getStatement(s.next).visitSuccessors(tmpAxioms); } }
	 */

	public int getLabel() {
		return label;
	}

	public static boolean isSatisfiable(Collection<String> axioms) {
		
		boolean result= false;
		
		//Axioms are written into a file
		try{
		FileWriter fw = new FileWriter("C:\\Users\\Administrator\\Documents\\z3-sample\\createIt.smt2");		
		BufferedWriter bw = new BufferedWriter(fw);

		Iterator<String> it = axioms.iterator();
		
		while(it.hasNext()){
			String str = (String)it.next();
			bw.write(str+"\r\n");
		}
		bw.write("(check-sat)\r\n");
		bw.write("(model)");
		
		bw.flush();
		bw.close();
		
		}
		catch(Exception e){
			e.printStackTrace();
		}
		
		//Runs the z3 solver on the created file.
		// File locations are hard-coded , but they can changed if required.
		try {
	         final Process process = Runtime.getRuntime().exec(
	            "z3.exe /m /smtc c:\\Users\\Administrator\\Documents\\z3-sample\\createIt.smt2");
	         BufferedReader input = new BufferedReader(new InputStreamReader(process.getInputStream()));
	         
	         
	         String retStr = null;
	         if( (retStr = input.readLine()) != null ){
	        	 if(retStr.compareToIgnoreCase("sat") == 0){ // The axioms are satisfiable, return true;
	        		 result = true;
	        	 }
	         }	         
	      } catch (IOException e) {
	         e.printStackTrace();
	      }		
		  return result;
	}
	
	public static int getLastNum() {
		return last_num;
	}

	public static Statement getStatement(int label) {
		try {
			return statements.get(label);
		} catch (IndexOutOfBoundsException e) {
			// it's possible that this will supress bugs - consider debugging with the try commented
			return BunkStatement.getInstance();
		}
	}
	
	public static int len(String name){
		StoreValue temp = zigma.getStoreValue(name);
		return temp.getRef();
	}
	
	/**
	 * @param name - The name of the array variable
	 * @param expr - The index expression of the array
	 * @param axiomColl - The axioms that have been collected so far
	 * @return Boolean - True if the array access is satisfiable
	 */
	public static boolean getResult(String name, Expression expr,ArrayList<String> axiomColl ){
		
		if(zigma.getStoreValue(name)== null || zigma.getStoreValue(name).getRef() == 0){
			System.out.println("The variable "+name+" does not support array as per declaration" +
					"or it is not declared");
			System.exit(1);
		}
		
		ArrayList<String> axiomColl1 = new ArrayList<String>(axiomColl);
		axiomColl1.add("(declare-const "+name+" Int)");
		axiomColl1.add("(assert (< "+name+" 0))");
		
		//If the array accessing element is integer then following
		if(expr instanceof LValueInt){
			/*axiomColl1.add("(assert (<= "+name+" "+((LValueInt)expr).getValue()+"))");
			axiomColl1.add("(assert (>= "+name+" "+((LValueInt)expr).getValue()+"))");*/
			//Above is replaced by below
			
			axiomColl1.add("(assert (= "+name+" "+((LValueInt)expr).getValue()+"))");
			
			if(isSatisfiable(axiomColl1)){
				System.out.println("ArrayUnderBoundAccess");
				System.exit(1);
			}			
		}
		
		//if the array access is done through variable
		if(expr instanceof Variable){
			Variable temp = ((Variable)expr);
			String VariName = temp.getVariable();
			StoreValue value = zigma.getStoreValue(VariName);
			
			//If the variable is never declared !!!
			if(value == null){
				System.out.println("Compiler error: No Variable "+VariName+" defined");
				System.exit(1);
			}
			
			Expression IntLitExpr = value.getExpression();
			
			//The array access is done through a undefined variable which must be warned
			if(IntLitExpr instanceof UndefinedExpression){
				
				//if the Variable is undefined then we have to obtain all the axioms pertaining to that and determine if it is a safe access
				HashSet<ArithExpr> ValidRules = new HashSet<ArithExpr>(Statement.rules.getArrays());
				
				//This contains the expression which are finished looking into
				HashSet<Expression> Finished = new HashSet<Expression>();
				
				addAxiomsForExpression(axiomColl1, name, expr, Finished, ValidRules);
			}
			
			if(IntLitExpr instanceof LValueInt){
				int Intvalue = ((LValueInt)IntLitExpr).getValue();
				/*axiomColl1.add("(assert (<= "+name+" "+Intvalue+"))");
				axiomColl1.add("(assert (>= "+name+" "+Intvalue+"))");*/
				//Above is replaced by below
			
				axiomColl1.add("(assert (= "+name+" "+Intvalue+"))");
			}
			
			if(isSatisfiable(axiomColl1)){
				System.out.println("ArrayUnderBoundAccess at "+expr.toString()+" in "+name);
				System.exit(1);
			}	
		}
		
		
		if(expr instanceof ArrayRef){
			ArrayRef temp = (ArrayRef) expr;
			String variable_name = temp.getVariable();
			Expression index = temp.getIndexExpression();
			ArrayList<String> empty = new ArrayList<String>();
			
			//Called SAT solver
			if(Statement.getResult(variable_name, index,empty )){
				Expression indexValue = Statement.zigma.getLValueInt(index);
				
				if(indexValue instanceof LValueInt){
					Expression shouldBeArray = Statement.zigma.getStoreValue(variable_name).getExpression();
					if(! (shouldBeArray instanceof ArrayLitExpression)){
						System.out.println("There is no array for this variable - File Store - Method getLValueInt(Expression rhs) ");
						System.exit(1);
					}
					Expression toPrint = ((ArrayLitExpression)shouldBeArray).getExpressionAtIndex(((LValueInt)indexValue).getValue());
					
					if(toPrint instanceof UndefinedExpression){
						//Do Nothing. AT this point , array is accessed with an undefined Variable
						//Let it FAIL :)
					}
					
					if(toPrint instanceof LValueInt){
						int Intvalue = ((LValueInt)toPrint).getValue();
						axiomColl1.add("(assert (= "+name+" "+Intvalue+"))");
					}
				}
				
				if(indexValue instanceof UndefinedExpression){
					//Do nothing. At this point we only know that array reference at the index is okay since the access is within a range.
					//But we dont know about the value returned . Thats why we dont add any axiom string which will eventually make it fail.
				}
			}
			else
			{
				System.out.println("This array reference is Unsatisfiable at "+index.toString()+" in "+variable_name);
				System.exit(1);
			}
			
			if(isSatisfiable(axiomColl1)){
				System.out.println("ArrayUnderBoundAccess at "+expr.toString()+" in "+name);
				System.exit(1);
			}	
		}
		
		//If the array accessing element is integer then following
		ArrayList<String> axiomColl2 = new ArrayList<String>(axiomColl);
		axiomColl2.add("(declare-const "+name+" Int)");
		axiomColl2.add("(assert (>= "+name+" "+len(name)+"))");
		if(expr instanceof LValueInt){
			/*axiomColl2.add("(assert (<= "+name+" "+((LValueInt)expr).getValue()+"))");
			axiomColl2.add("(assert (>= "+name+" "+((LValueInt)expr).getValue()+"))");*/
			//Above is replaced by below
			
			axiomColl2.add("(assert (= "+name+" "+((LValueInt)expr).getValue()+"))");
			
			if(isSatisfiable(axiomColl2)){
				System.out.println("ArrayOverBoundAccess");
				System.exit(1);
			}			
		}
		
		//if the array access is done through variable
		//PART-1
		/*if(expr instanceof Variable){
			Variable temp = ((Variable)expr);
			String VariName = temp.getVariable();
			StoreValue value = zigma.getStoreValue(VariName);
			Expression IntLitExpr = value.getExpression();
			if(IntLitExpr instanceof UndefinedExpression){//The array access is done through a undefined variable which must be warned
				System.out.println("The array indexing is done through an undefined variable which is never safe"); 
				System.exit(1);
			}
			int Intvalue = ((LValueInt)IntLitExpr).getValue();
			/*axiomColl2.add("(assert (<= "+name+" "+Intvalue+"))");
			axiomColl2.add("(assert (>= "+name+" "+Intvalue+"))");*/
			//Above is replaced by below
			
		//PART-2
			/*axiomColl2.add("(assert (= "+name+" "+Intvalue+"))");
			
			if(isSatisfiable(axiomColl2)){
				System.out.println("ArrayOverBoundAccess at"+expr.toString()+" in "+name);
				System.exit(1);
			}	
		}*/
		//The above is replaced by below
		
		//if the array access is done through variable
		if(expr instanceof Variable){
			Variable temp = ((Variable)expr);
			String VariName = temp.getVariable();
			StoreValue value = zigma.getStoreValue(VariName);
			
			//If the variable is never declared !!!
			if(value == null){
				System.out.println("Compiler error: No Variable "+VariName+" defined");
				System.exit(1);
			}
			
			Expression IntLitExpr = value.getExpression();
			
			//The array access is done through a undefined variable which must be warned
			if(IntLitExpr instanceof UndefinedExpression){
				
				//if the Variable is undefined then we have to obtain all the axioms pertaining to that and determine if it is a safe access
				HashSet<ArithExpr> ValidRules = new HashSet<ArithExpr>(Statement.rules.getArrays());
				
				//This contains the expression which are finished looking into
				HashSet<Expression> Finished = new HashSet<Expression>();
				
				addAxiomsForExpression(axiomColl2, name, expr, Finished, ValidRules);
			}
			
			if(IntLitExpr instanceof LValueInt){
				int Intvalue = ((LValueInt)IntLitExpr).getValue();
				/*axiomColl1.add("(assert (<= "+name+" "+Intvalue+"))");
				axiomColl1.add("(assert (>= "+name+" "+Intvalue+"))");*/
				//Above is replaced by below
			
				axiomColl2.add("(assert (= "+name+" "+Intvalue+"))");
			}
			
			if(isSatisfiable(axiomColl2)){
				System.out.println("ArrayOverBoundAccess at "+expr.toString()+" in "+name);
				System.exit(1);
			}	
		}
		
		if(expr instanceof ArrayRef){
			ArrayRef temp = (ArrayRef) expr;
			String variable_name = temp.getVariable();
			Expression index = temp.getIndexExpression();
			ArrayList<String> empty = new ArrayList<String>();
			
			//Called SAT solver
			if(Statement.getResult(variable_name, index,empty )){
				Expression indexValue = Statement.zigma.getLValueInt(index);
				
				if(indexValue instanceof LValueInt){
					Expression shouldBeArray = Statement.zigma.getStoreValue(variable_name).getExpression();
					if(! (shouldBeArray instanceof ArrayLitExpression)){
						System.out.println("There is no array for this variable - File Store - Method getLValueInt(Expression rhs) ");
						System.exit(1);
					}
					Expression toPrint = ((ArrayLitExpression)shouldBeArray).getExpressionAtIndex(((LValueInt)indexValue).getValue());
					
					if(toPrint instanceof UndefinedExpression){
						//Do Nothing. AT this point , array is accessed with an undefined Variable
						//Let it FAIL :)
					}
					
					if(toPrint instanceof LValueInt){
						int Intvalue = ((LValueInt)toPrint).getValue();
						axiomColl2.add("(assert (= "+name+" "+Intvalue+"))");
					}
				}
				
				if(indexValue instanceof UndefinedExpression){
					//Do nothing. At this point we only know that array reference at the index is okay since the access is within a range.
					//But we dont know about the value returned . Thats why we dont add any axiom string which will eventually make it fail.
				}
			}
			else
			{
				System.out.println("This array reference is Unsatisfiable at "+index.toString()+" in "+variable_name);
				System.exit(1);
			}
			
			if(isSatisfiable(axiomColl2)){
				System.out.println("ArrayOverBoundAccess at "+expr.toString()+" in "+name);
				System.exit(1);
			}	
		}
		
		return true;
	}
	
	public static void addAxiomsForExpression(ArrayList<String> axioms,
			String name, Expression currExpr, HashSet<Expression> finished, HashSet<ArithExpr> ValidRules) {
		// TODO Auto-generated method stub
		
		//Sometime repetition , but does not matter
		finished.add(currExpr);
		axioms.add("(declare-const "+name+" Int)");
		
		Iterator<ArithExpr> itRuleSet = ValidRules.iterator();
		HashSet<ArithExpr> UpToDate = new HashSet<ArithExpr>(ValidRules);
		
			
		while(itRuleSet.hasNext()){
			ArithExpr currentRule = itRuleSet.next();
			UpToDate.remove(currentRule);
			
			currentRule.addAxiomsForExpression(axioms,currExpr,name,finished, new HashSet<ArithExpr>(UpToDate));
		}//end- while(it.hasNext())
		
		finished.remove(currExpr);
		
	}

	public static void processLabels(Map<String, Integer> labels) throws InstantiationException {
		for(Statement s : statements) {
			if(s.labelName != null) {
				Integer lineNumber = labels.get(s.labelName);
				if(lineNumber == null) {
					throw new InstantiationException("Could not find label " + s.labelName);
				} else {
					s.label = lineNumber;
				}
			}
		}
	}
	
	/**
	 * @author Petey
	 * Ensures that the last statement is the BunkStatement.
	 * This simplifies the graph search because visitSuccessors()
	 * returns immediately. It also guarantees that there won't be
	 * a dangling label at the end.
	 */
	public static void doneWithStatements() {
		statements.add(BunkStatement.getInstance());
	}

	/**
	 * This method tells whether this branching can be executed or pruned.
	 * @param left - Says if the left expression should be included in the Z3 solver
	 * @param right - Says if the right expression should be included in the Z3 solver
	 * @return - returns the Z3 result
	 */
	public static boolean canBranch(ArithExpr actualRule) {
		
		//This array will contain all the statements to be supplied to Z3
		ArrayList<String> rulesString= new ArrayList<String>(); 
		
		String addIt = "(assert ("+actualRule.getOper();
		
		//For the LHS
		Expression conditionLHS = actualRule.getLHS();
		Expression LHS = Statement.zigma.getLValueInt(conditionLHS);
		if(LHS instanceof LValueInt){
			addIt = addIt+((LValueInt)LHS).getValue()+" ";
		}
		if(LHS instanceof UndefinedExpression){
			addIt = addIt +(conditionLHS.toString())+" ";
			HashSet<ArithExpr> ValidRules = new HashSet<ArithExpr>(Statement.rules.getArrays());
			HashSet<Expression> Finished = new HashSet<Expression>();
			addAxiomsForExpression(rulesString, conditionLHS.toString(), conditionLHS, Finished, ValidRules);
		}
		
		//For RHS
		Expression conditionRHS = actualRule.getRHS();
		Expression RHS = Statement.zigma.getLValueInt(conditionRHS);
		if(RHS instanceof LValueInt){
			addIt = addIt+((LValueInt)RHS).getValue()+"))";
		}
		if(RHS instanceof UndefinedExpression){
			addIt = addIt+(conditionRHS.toString())+"))";
			HashSet<ArithExpr> ValidRules = new HashSet<ArithExpr>(Statement.rules.getArrays());
			HashSet<Expression> Finished = new HashSet<Expression>();
			addAxiomsForExpression(rulesString, conditionRHS.toString(), conditionRHS, Finished, ValidRules);
		}
		
		rulesString.add(addIt);
		return isSatisfiable(rulesString);
		
		
		/*//set the iterator for the rules array
		Iterator<ArithExpr> it = Statement.rules.getArrays().iterator();
		
		//This array will contain all the statements to be supplied to Z3
		ArrayList<String> rulesString= new ArrayList<String>(); 
		
		//Loop through the different rules one-by-one
		while(it.hasNext()){
			
			//Current points to the rule
			ArithExpr current = it.next();
			
			//get the left expression
			Expression left = current.getLHS();
			
			if(!createAxioms(rulesString, left)){
				//If the axioms cannot be made then quit
				System.out.println("Axioms cannot be generated");
				System.exit(1);
			}
			
			//get the right expression
			Expression right = current.getRHS();
			
			if(!createAxioms(rulesString, right)){
				//If the axioms cannot be made then quit
				System.out.println("Axioms cannot be generated");
				System.exit(1);
			}
			
			//Add the relation of the axiom to the set of the arrays
			rulesString.add(current.getAxiomString());		
		}
		
		//Satisfiablility i.e. the return value says if the branch 
		//should be pruned or not. 
		return isSatisfiable(rulesString);*/
	}
	
	/*public static boolean createAxioms(ArrayList<String> axiomSet, Expression e){
		if(e instanceof UndefinedExpression){
			return false;
		}
		
		if(e instanceof LValueInt){
			//Do Nothing. But still the comparison is valid
			return true;
		}
		
		if(e instanceof Variable){
			Variable temp = (Variable)e;
			String VariName = temp.getVariable();
			StoreValue value = zigma.getStoreValue(VariName);
			Expression IntLitExpr = value.getExpression();
			if(IntLitExpr instanceof UndefinedExpression){//The array access is done through a undefined variable which must be warned
				System.out.println("The array indexing is done through an undefined variable which is never safe"); 
				System.exit(1);
			}
			int Intvalue = ((LValueInt)IntLitExpr).getValue();

			axiomSet.add("(declare-const "+VariName+" Int)");
			axiomSet.add("(assert (<= "+VariName+" "+Intvalue+"))");
			axiomSet.add("(assert (>= "+VariName+" "+Intvalue+"))");
			//Above is replaced by below
			
			axiomSet.add("(assert (= "+VariName+" "+Intvalue+"))");
		}
		
		if(e instanceof ArrayRef){
			ArrayRef temp = (ArrayRef)e;
			
			//condition is array validity - solver 
			if(getResult(temp.getVariable(), temp.getIndexExpression(), null)){
				
				// Body - for the value inside the array reference
				String VariableName = temp.getVariable();
				if(temp.getIndexExpression() instanceof LValueInt){
					VariableName = VariableName + ((LValueInt)(temp.getIndexExpression())).getValue();
				}
				if(temp.getIndexExpression() instanceof Variable){
					VariableName = VariableName + ((Variable)(temp.getIndexExpression())).getVariable();
				}
				
				//Check THIS STATEMENT//int Intvalue = (Statement.zigma.getLValueInt(temp)).getValue();

				axiomSet.add("(declare-const "+VariableName+" Int)");
				axiomSet.add("(assert (<= "+VariableName+" "+Intvalue+"))");
				axiomSet.add("(assert (>= "+VariableName+" "+Intvalue+"))");
				//Above is replaced by below
				
				//Check THIS STATEMENT//axiomSet.add("(assert (= "+VariableName+" "+Intvalue+"))");
				
			}
		}
		return true;
	}*/
}
